Refining the control structure of loops using static analysis

ABSTRACT

We present a simple yet useful technique for refining the control structure of loops that occur in imperative programs. Loops containing complex control flow are common in synchronous embedded controllers derived from modeling languages such as Lustre, Esterel, and Simulink/Stateflow. Our approach uses a set of labels to distinguish different control paths inside a given loop. The iterations of the loop are abstracted as a finite state automaton over these labels. Subsequently, we use static analysis techniques to identify infeasible iteration sequences and subtract such forbidden sequences from the initial language to obtain a refinement. In practice, the refinement of control flow sequences often simplifies the control flow patterns in the loop. We have applied the refinement technique to improve the precision of abstract interpretation in the presence of widening. Our experiments on a set of complex reactive loop benchmarks clearly show the utility of our refinement techniques. Abstraction interpretation with our refinement technique was able to verify all the properties for 10 out of the 13 benchmarks, while abstraction interpretation without refinement was able to verify only four. Other potentially useful applications include termination analysis and reverse engineering models from source code.

References

1. Absint WCET timing analysis tool. http://www.absint.com/.
2. Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. In Static Analysis Symposium (2003), vol. 2694 of LNCS, Springer, pp. 337--354.
3. Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Wei, O., and Gupta, A. SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. In SAS (2008), vol. 5079 of LNCS, pp. 238--254.
4. Ball, T., and Rajamani, S. K. The SLAM toolkit. In CAV (2001), vol. 2102 of LNCS, pp. 260--264.
5. Bardin, S., Finkel, A., Leroux, J., and Petrucci, L. FAST: Fast accelereation of symbolic transition systems. In CAV (July 2003), vol. 2725 of LNCS.
6. Beyer, D., Henzinger, T. A., Jhala, R., and Majumdar, R. The software model checker BLAST. STTT 9, 5-6 (2007), 505--525.
7. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., and Rival, X. A static analyzer for large safety-critical software. In PLDI (June 2003), pp. 196--207.
8. Clarke, E., Kroening, D., and Lerda, F. A tool for checking ANSI-C programs. In TACAS (2004), vol. 2988 of LNCS.
9. Colon, M., Sankaranarayanan, S., and Sipma, H. Linear invariant generation using non-linear constraint solving. In CAV (July 2003), vol. 2725 of LNCS, Springer, pp. 420--433.
10. Colon, M., and Sipma, H. Synthesis of linear ranking functions. In Tools and Algorithms for Construction and Analysis of Systems (April 2001), vol. 2031 of LNCS.
11. Cook, B., Podelski, A., and Rybalchenko, A. Termination proofs for systems code. In PLDI (2006).
12. Cousot, P., and Cousot, R. Static determination of dynamic properties of programs. In Proc. ISOP'76 (1976), Dunod, Paris, France, pp. 106--130.
13. Cousot, P., and Cousot, R. Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL (1977), pp. 238--252.
14. Cousot, P., and Halbwachs, N. Automatic discovery of linear restraints among the variables of a program. In POPL'78 (Jan. 1978), pp. 84--97.
15. Esparza, J., Hansel, D., Rossmanith, P., and Schwoon, S. Efficient algorithms for model checking pushdown systems. In CAV (2000), vol. 1855 of LNCS.
16. Fehnker, A., Brauer, J., Huuck, R., and Seefried, S. Goanna: Syntactic software model checking. In Auto. Tech. for Verif.&Analysis (2008).
17. Gaubert, S., Goubault, E., Taly, A., and Zennou, S. Static analysis by policy iteration on relational domains. In ESOP (2007), vol. 4421 of LNCS, pp. 237--252.
18. Gawlitza, T., and Seidl, H. Precise fixpoint computation through strategy iteration. In ESOP (2007), vol. 4421 of LNCS, pp. 300--315.
19. Gopan, D., and Reps, T. W. Lookahead widening. In CAV (2006), vol. 4144 of LNCS, pp. 452--466.
20. Gopan, D., and Reps, T. W. Guided static analysis. In SAS (2007), vol. 4634 of LNCS, pp. 349--365.
21. Goubault, E., and Putot, S. Static analysis of numerical algorithms. In SAS (2006), vol. 4134 of LNCS, Springer, pp. 18--34.
22. Gulwani, S., Jain, S., and Koskinen, E. Control-flow refinement and progress invariants for bound analysis. PLDI 2009 (to appear).
23. Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., and Xu, R.-G. Proving non-termination. In POPL (2008), ACM, pp. 147--158.
24. Halbwachs, N. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993.
25. Halbwachs, N., Proy, Y., and Roumanoff, P. Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11, 2 (1997), 157--185.
26. Harary, F. Graph Theory. Addison-Wesley, 1969.
27. Ivancic, F., Yang, Z., Ganai, M. K., Gupta, A., Shlyakhter, I., and Ashar, P. F-soft: Software verification platform. In CAV (2005), vol. 3576 of LNCS.
28. Jeannet, B., Halbwachs, N., and Raymond, P. Dynamic partitioning in analyses of numerical properties. In Static Analysis Symposium, SAS'99 (Sep 1999), vol. 1694 of LNCS, pp. 39--50.
29. MathWorks Inc. Electronic vehicle climate control simulink/stateflow model. www.mathworks.com/products/simulink/demos.html.
30. Mathworks Inc. Simulink/stateflow (tm) model-based control design environment. Cf. www.mathworks.com/simulink.
31. Mauborgne, L., and Rival, X. Trace partitioning in abstract interpretation based static analyzers. In ESOP (2005), vol. 3444 of LNCS, pp. 5--20.
32. Min´e, A. A new numerical abstract domain based on difference-bound matrices. In PADO II (May 2001), vol. 2053 of LNCS, Springer, pp. 155--172.
33. Sankaranarayanan, S., Ivancic, F., and Gupta, A. Program analysis using symbolic ranges. In SAS (2007), vol. 4634 of LNCS, pp. 366--383.
34. Sankaranarayanan, S., Ivancic, F., Shlyakhter, I., and Gupta, A. Static analysis in disjunctive numerical domains. In SAS (2006), vol. 4134 of LNCS.
35. Simon, A., and King, A. Widening polyhedra with landmarks. In APLAS (2006), vol. 4279 of LNCS.

Index Terms

• Hardware

  • Hardware validation

    • Functional verification

      • Assertion checking

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Model checking

• Theory of computation

  • Logic

    • Verification by model checking

  • Semantics and reasoning

    • Program reasoning

      • Assertions

      • Program analysis

    • Program semantics